/*
 * PosCSParser.cpp
 *
 * Copyright 2013 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/PosCSParser.hpp"

using std::string;

namespace bfr {

PosCSParser::PosCSParser()
    : variableCount(-1), clauseCount(-1), clauses(), type(UNKNOWN) { }

PosCSParser::~PosCSParser() { }

const char PosCSParser::COMMENT_CHAR = 'c';
const char PosCSParser::PROBLEM_CHAR = 'p';

const char PosCSParser::CNF_PROBLEM[] = "cnf";

const char PosCSParser::MINUS = '-';

bool PosCSParser::isLineEmpty(const string &line) const {
    return (line.find_first_not_of(" \t") == std::string::npos);
}

size_t PosCSParser::parseNumber(string &line, size_t *pos) throw(string) {
    // search for the next space that terminates the number
    size_t nextSpace = line.find(' ', *pos);
    if (nextSpace == string::npos) {
            // there is no " ". So we assume the the rest of the
            // line is the whole number
            nextSpace = line.size();
    }
    // get the substring
    size_t len = nextSpace - *pos;
    string substr = line.substr(*pos, len);
    try {
            *pos = nextSpace + 1;
            return boost::lexical_cast<size_t>( substr );
    }
    catch (const boost::bad_lexical_cast &e ) {
            throw string("Can't parse ") + substr + " as number.";
    }
}

void PosCSParser::readProblemLine(string &line) throw(string) {
        // we know that the line starts with "p"
        // find the first pos where we expect the variable number

        if (line.size() <= 3) {
            throw string("Expected \"p PROBLEM_INSTANCE (aka cnf)\"."
                                   "But found only \"" + line + "\".");
        }

        if (line[1] != ' ') {
                throw string("Expected BLANK after \"p\", but found \"p")
                        + line[1] +std::string("\".");
        }

        size_t pos = 2;
        // assume that now we have
        // "PROBLEM_TYPE VARIABLES CLAUSES"

        // find the next whitespace starting at pos 2 (end of the problem type)
        size_t nextSpace = line.find(' ', pos);
        // get the substring
        string problemType = line.substr(pos, nextSpace - pos);
        // set the global type
        if (problemType.compare(PosCSParser::CNF_PROBLEM) == 0) {
                type = PosCSParser::problem_type::CNF;
        }
        else {
                type = PosCSParser::problem_type::UNKNOWN;
        }
        // move from space to next char
        pos = nextSpace + 1;
        try {
                variableCount = parseNumber(line, &pos);
                clauseCount = parseNumber(line, &pos);
                clauses = PosCS(clauseCount);
        }
        catch(string &e) {
                throw e;
        }
}

void PosCSParser::readClause(string &line, bool sort) throw(string) {
    const size_t clauseID = clauses.addClause();

    size_t pos = 0;
    size_t id = -1;
    // read clauses until we have "0"
    do {
        // we actually ignore the polarity, maybe print a warning or something...
        //bool polarity = true;
        if (line[pos] == PosCSParser::MINUS) {
            //polarity = false;
            ++pos;
        }
        try {
            id = parseNumber(line, &pos);
            if (id != 0) {
                clauses.getClause(clauseID).push_back(id - 1);
            }
        }
        catch (const string &str) {
            throw str;
        }
    } while (id != 0);
    if (sort) {
        clauses.sortClause(clauseID);
    }
}

size_t PosCSParser::getVariableCount() const {
    return variableCount;
}

PosCS PosCSParser::parse(std::istream &in, bool sortClause) throw(string) {
        string line;
        if (!in.good()) {
            throw std::string("Can't parse DIMACS DNF from stream.");
        }
        do {
            getline(in, line);
            if (in.eof()) {
                throw string("Can't parse DIMACS DNF from stream.");
            }
        } while ((line[0] == COMMENT_CHAR) || isLineEmpty(line));


        // now expecting the comment line
        if ((line.size() == 0) || (line[0] != PROBLEM_CHAR)) {
            throw string("Missing problem line in DIMACS input.");
        }
        try {
            readProblemLine(line);
        }
        catch (string &e) {
            throw e;
        }

        for (size_t i = 0; i < clauseCount;) {
            if (in.eof()) {
                throw string("Input does not define as many clauses as "
                        "defined in problem line.");
            }
            getline(in, line);
            if ((line.size() == 0) || (line[0] == COMMENT_CHAR)) {
                continue;
            }
            try {
                    readClause(line, sortClause);
                    i++;
                }
                catch (string &e) {
                    throw e;
                }
        }
        return clauses;
}

}


